$\forall$$T$:Type, $L$:$T$ List, $i$, $j$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$. $\parallel$swap($L$;$i$;$j$)$\parallel$ $=$ $\parallel$$L$$\parallel$ $\in$ $\mathbb{Z}$